Inference at * 1 2 1 2 
Iof proof for Lemma fast-fib:



1. n : 
2. 0 < n
3. a, b:.
3. {m:| 
3. {k:.
3. {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib((n - 1)+k))} 
4. a : 
5. b : 
6. b1:.
6. {m:| 
6. {k:.
6. {(a+b = fib(k))
6. { ((k  0)  (b1 = 0))
6. { ((0 < k)  (b1 = fib(k - 1)))
6. { (m = fib((n - 1)+k))} 
7. {m:| 
7. {k:.
7. {(a+b = fib(k))
7. { ((k  0)  (a = 0))
7. { ((0 < k)  (a = fib(k - 1)))
7. { (m = fib((n - 1)+k))} 
  {m:| 
  {k:.
  {(a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))}  

latex

 by (D (-1)) 
CollapseTHEN ((InstConcl [m]) 
CollapseTHEN ((Auto) 
CollapseTHEN (Auto')))
C 

latex

C1: 

C1: 7. m : 
C1: 8. k:.
C1: 8. (a+b = fib(k))
C1: 8.  ((k  0)  (a = 0))
C1: 8.  ((0 < k)  (a = fib(k - 1)))
C1: 8.  (m = fib((n - 1)+k))
C1: 9. k : 
C1: 10. a = fib(k)
C1: 11. (k  0)  (b = 0)
C1: 12. (0 < k)  (b = fib(k - 1))
C1:   m = fib(n+k)
C.

Definitions	, s = t, -n, n - m, , A, False, Void, a < b, fib(n), A  B, #$n, P  Q, n+m, x:A. B(x), x:AB(x), t  T, , {x:A| B(x)}
Lemmas	nat wf, fib wf, le wf